Require Import ZArith.
Open Scope Z_scope.

Inductive reg : Set :=	(* registers *)
  | esp : reg
  | ebp : reg
  | eax : reg
  | ebx : reg
  | ecx : reg
  | edx : reg
  | esi : reg
  | edi : reg.


Definition beq_reg (r1 r2 : 	(* comp r1 r2, ret bool *)
                    reg) :=
  match r1, r2 with
  | esp, esp => true
  | ebp, ebp => true
  | eax, eax => true
  | ebx, ebx => true
  | ecx, ecx => true
  | edx, edx => true
  | esi, esi => true
  | edi, edi => true
  | _, _ => false
  end.

Inductive rfile : Set :=	(* register file *)
  | emptyR : rfile
  | consR : rfile -> reg -> Z -> rfile.

Fixpoint lookupR (rf : rfile) (r : reg) {struct rf} : Z :=
  	(* look up reg file *)
 match rf with
 | emptyR => 0
 | consR rf' r' i => if beq_reg r r' then i else lookupR rf' r
 end.

Definition updateR (rf : rfile) (r : reg) (i : Z) : rfile :=
   (* update reg file *)
  consR rf r i.

Definition heap:Set := Z->Z.
Definition hr(h:heap)(a:Z):Z := h a.
Definition hw(h:heap)(a:Z)(v:Z):Z->Z := fun (a1:Z) =>
  if (Zeq_bool a a1) then v else (h a1).

Lemma w1: forall h a v, hr (hw h a v) a = v.
Proof.
  intros.
  unfold hr; unfold hw.
  unfold Zeq_bool. 
  rewrite (Zcompare_refl a).
  reflexivity.
Qed.

Lemma w2: forall h a a1 v, a<>a1 ->  hr (hw h a v) a1 = h a1. 
Proof.
  intros.
  unfold hr; unfold hw.
  unfold Zeq_bool.
  assert (Hz := Ztrichotomy_inf a a1).
  destruct Hz as [[z | z] | z];
    try (rewrite z; reflexivity).
  subst a.
  elimtype False.
  apply H; reflexivity.
Qed.

